package trabajoISW2.domain.contracts;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Book;

@Inv({"getItemId()>=0"})
public interface IDetail {
	
	@Pre("itemId >= 0 && itemId <= Integer.MAX_VALUE #WrongIdException")
	@Pos("getItemId() == itemId")
	public void setDetailId (int itemId);
	
	@Query
	public int getDetailId();
	
	@Pre("quantity > 0 && quantity <= 99 #NoPositiveNumberException")
	@Pos("getQuantity() == quantity")
	public void setQuantity(int quantity);
	
	@Query
	public int getQuantity();
	
	@Pre({"book != null #IllegalArgumentException"})
	@Pos({"getBook().compare(book) == 0"})
	public void setBook(Book book);
	
	@Query
	public Book getBook();
	


}
